PACKAGE BODY DivRest IS

   PROCEDURE DivRestBis (X: IN out Integer; Y: IN Integer; D: out Integer) IS
      S: Integer;
      P: Integer;
   BEGIN
      --#PRE: X = X_anf AND X_anf >= 0 AND Y = Y_anf AND Y_anf > 0
      D := 0;
      S := Y;
      P := 1;
      --#BOUND: X-(S/2)
      --#INV1: X >= 0 AND Y > 0 AND Y = Y_anf AND S = (P*Y) AND D = 0 AND P >= 1
      WHILE X >= S LOOP
         S := (S*2);
         P := (P*2);
      END LOOP;
      --#BOUND: (X-Y)+1
      --#INV2: X >= 0 AND Y = Y_anf AND Y_anf > 0 AND X_anf = ((D*Y)+X) AND S = (P*Y) AND ((P >= 1 AND X < Y) OR (P > 1 AND X >= Y))
      WHILE X >= Y LOOP
         --#BOUND: (S*2)-X
         --#INV3: X >= Y AND Y = Y_anf AND Y_anf > 0 AND X_anf = ((D*Y)+X) AND S = (P*Y) AND P > 1
         WHILE X < S LOOP
            S := (S/2);
            P := (P/2);
         END LOOP;
         D := (D+P);
         X := (X-S);
      END LOOP;
      --#POST: X_anf = ((D*Y_anf)+X) AND X >= 0 AND X < Y_anf
   END DivRestBis;

   PROCEDURE DivRestLin (X, Y: IN OUT Integer) IS
      D: Integer;
   BEGIN
      --#PRE: X = X_anf AND Y = Y_anf AND X_anf >= 0 AND Y_anf > 0
      D := 0;
      --#BOUND: X-Y
      --#INV: X_anf = ((D*Y_anf)+X) AND X >= 0 AND Y = Y_anf AND Y_anf > 0
      WHILE X >= Y LOOP
         D := (D+1);
         X := (X-Y);
      END LOOP;
      --#POST: X_anf = ((D*Y_anf)+X) AND X >= 0 AND X < Y_anf
   END DivRestLin;

END DivRest;